Inference at * 1 2 2 
Iof proof for Lemma adjacent-cons:



1. T : Type
2. x : T
3. y : T
4. u : T
5. L : T List
6. i : {0..((||L||+1) - 1)}
7. x = [u / L][i]
8. y = [u / L][(i+1)]
9. 0 < ||L||
10. (i = 0)
  y = L[((i - 1)+1)] 

latex

 by InteriorProof ((((RWO "select_cons_tl" (-3)) 
THENM (All ArithSimp))) 
TCollapseTHEN (Auto))
TCollapseTHEN (Auto

latex

TC.

Definitions	P  Q, P  Q, , x:A. B(x), T, x:AB(x), Void, True, l[i], [car / cdr], t  T, x:A  B(x), #$n, s = t, type List, Type, {i..j}, {x:A| B(x)} , , i  j < k, A  B, P & Q, A, False, P  Q, a < b, n - m, n+m, ||as||
Lemmas	iff wf, rev implies wf, select cons tl, length wf1, int seg wf, true wf, le wf, squash wf, select wf